The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
append(cons(y, ys), x) →⁺ cons(y, append(ys, x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [ys / cons(y, ys)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0') → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0')) → 0'
p(0') → 0'
inc(s(x)) → s(inc(x))
inc(0') → s(0')
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0') → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0')) → 0'
p(0') → 0'
inc(s(x)) → s(inc(x))
inc(0') → s(0')
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

Types:
isEmpty :: cons:nil:differentLengthError → false:true
cons :: 0':s → cons:nil:differentLengthError → cons:nil:differentLengthError
false :: false:true
nil :: cons:nil:differentLengthError
true :: false:true
isZero :: 0':s → false:true
0' :: 0':s
s :: 0':s → 0':s
head :: cons:nil:differentLengthError → 0':s
tail :: cons:nil:differentLengthError → cons:nil:differentLengthError
append :: cons:nil:differentLengthError → 0':s → cons:nil:differentLengthError
p :: 0':s → 0':s
inc :: 0':s → 0':s
addLists :: cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError
if :: false:true → false:true → false:true → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError
hole_false:true1_0 :: false:true
hole_cons:nil:differentLengthError2_0 :: cons:nil:differentLengthError
hole_0':s3_0 :: 0':s
gen_cons:nil:differentLengthError4_0 :: Nat → cons:nil:differentLengthError
gen_0':s5_0 :: Nat → 0':s

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
append, p, inc, addLists

They will be analysed ascendingly in the following order:
append < addLists
p < addLists
inc < addLists

(8) Obligation:

TRS:
Rules:
isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0') → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0')) → 0'
p(0') → 0'
inc(s(x)) → s(inc(x))
inc(0') → s(0')
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

Types:
isEmpty :: cons:nil:differentLengthError → false:true
cons :: 0':s → cons:nil:differentLengthError → cons:nil:differentLengthError
false :: false:true
nil :: cons:nil:differentLengthError
true :: false:true
isZero :: 0':s → false:true
0' :: 0':s
s :: 0':s → 0':s
head :: cons:nil:differentLengthError → 0':s
tail :: cons:nil:differentLengthError → cons:nil:differentLengthError
append :: cons:nil:differentLengthError → 0':s → cons:nil:differentLengthError
p :: 0':s → 0':s
inc :: 0':s → 0':s
addLists :: cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError
if :: false:true → false:true → false:true → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError → cons:nil:differentLengthError → cons:nil:differentLengthError
hole_false:true1_0 :: false:true
hole_cons:nil:differentLengthError2_0 :: cons:nil:differentLengthError
hole_0':s3_0 :: 0':s
gen_cons:nil:differentLengthError4_0 :: Nat → cons:nil:differentLengthError
gen_0':s5_0 :: Nat → 0':s

Generator Equations:
gen_cons:nil:differentLengthError4_0(0) ⇔ nil
gen_cons:nil:differentLengthError4_0(+(x, 1)) ⇔ cons(0', gen_cons:nil:differentLengthError4_0(x))
gen_0':s5_0(0) ⇔ 0'
gen_0':s5_0(+(x, 1)) ⇔ s(gen_0':s5_0(x))

The following defined symbols remain to be analysed:
append, p, inc, addLists

They will be analysed ascendingly in the following order:
append < addLists
p < addLists
inc < addLists